Doctoral Thesis - Modelling Memory Consistency Models for Formal Verification